RCS "$Id: HMLSat.sig,v 1.5 1998/08/13 11:38:48 pxs Exp $";
(********************************** HMLSat ***********************************)
(*                                                                           *)
(* This file contains the signature for local model checking.                *)
(*                                                                           *)
(*****************************************************************************)

signature HMLSAT =
sig
(*    type act *)
(*    type agent *)
  type prop 
  structure Ag : AGENT_WRAPPER

(*   val check : (agent -> (act * agent) list) -> agent -> prop -> bool *)
  val check : (Ag.agent -> (Ag.A.act * Ag.agent) list) -> Ag. agent -> prop
    -> bool
end

